package dpll.fnc;

import static org.junit.Assert.assertEquals;

import java.io.IOException;
import java.io.StringReader;

import org.antlr.v4.runtime.ANTLRInputStream;
import org.antlr.v4.runtime.CommonTokenStream;
import org.junit.Test;

import dpll.ast.ASTVisitor;
import dpll.ast.IASTNode;
import dpll.parser.logpropBaseVisitor;
import dpll.parser.logpropLexer;
import dpll.parser.logpropParser;
import dpll.parser.logpropParser.FormulasContext;

public class FNCTransformTest {
	
	private String a = "a1";
	private String b = "b1";
	private String c = "c1";
	
    @Test
    public void doubleNegation() throws IOException {
            //assertTransform("not not a", "(atom a)");
    	String entrada = "NO NO " + a + ";";
    	String equivalente = a + ";";
        
        assertEquals(transforma(entrada), transforma(equivalente));
    }
    
    @Test
    public void tripleNegation() throws IOException {
            //assertTransform("not not not a", "(not (atom a))");
    	String entrada = "NO NO NO " + a + ";";
    	String equivalente = "NO " + a + ";";
        
        assertEquals(transforma(entrada), transforma(equivalente));	
    }
    
    @Test
    public void quadNegation() throws IOException {
            //assertTransform("not not not not a", "(atom a)");
    	String entrada = "NO NO NO NO " + a + ";";
    	String equivalente = a + ";";
        
        assertEquals(transforma(entrada), transforma(equivalente));
    }
    
    @Test
    public void conditional() throws IOException {
            //assertTransform("a then b", "(or (not (atom a)) (atom b))");
    	String entrada = a + " SI " + b  + ";";
    	String equivalente = "NO " + a + " O " + b + ";";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }
    
    @Test
    public void iff() throws Exception {
            //assertTransform("a iff b", "(and (or (not (atom a)) (atom b)) (or (not (atom b)) (atom a)))");
    	String entrada = a + " SISOLOSI " + b  + ";";
    	String equivalente = "(NO " + a + " O " + b + ") Y (NO " + b + " O " + a +  ");";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }
    
    @Test
    public void morganAnd() throws Exception {
            //assertTransform("not (a and b)", "(or (not (atom a)) (not (atom b)))");
    	String entrada = "NO (" + a + " Y " + b +  ");";
    	String equivalente = "NO " + a + " O NO " + b +  ";";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }
    
    @Test
    public void morganOr() throws Exception {
            //assertTransform("not (a or b)", "(and (not (atom a)) (not (atom b)))");
    	String entrada = "NO (" + a + " O " + b +  ");";
    	String equivalente = "NO " + a + " Y NO " + b +  ";";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }   
    
    @Test
    public void distributivityOrOverAndRight() throws Exception {
            //assertTransform("f or (g and h)", "(and (or (atom f) (atom g)) (or (atom f) (atom h)))");
    	String entrada = a + " O " + b + " Y " + c +  ";";
    	String equivalente = "(" + a + " O " + b + ") Y (" + a + " O " + c +  ");";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }
    
    @Test
    public void distributivityOrOverAndLeft() throws Exception {
            //assertTransform("(f and g) or h", "(and (or (atom f) (atom h)) (or (atom g) (atom h)))");
    	String entrada = a + " Y " + b + " O " + c +  ";";
    	String equivalente = "(" + a + " O " + c + ") Y (" + b + " O " + c +  ");";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }
    
    @Test
    public void booleanAndTrueLeft() throws Exception {
            //assertTransform("true and a", "(atom a)");
    	String entrada = "TRUE Y " + a +  ";";
    	String equivalente = a +  ";";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }

    @Test
    public void booleanAndFalseLeft() throws Exception {
            //assertTransform("false and a", "false");
    	String entrada = "FALSE Y " + a +  ";";
    	String equivalente = "FALSE;";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }

    @Test
    public void booleanAndTrueRight() throws Exception {
            //assertTransform("a and true", "(atom a)");
    	String entrada =  a + " Y TRUE;";
    	String equivalente = a +  ";";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }

    @Test
    public void booleanAndFalseRight() throws Exception {
            //assertTransform("a and false", "false");
    	String entrada =  a + " Y FALSE;";
    	String equivalente = "FALSE;";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }
    
    @Test
    public void booleanOrTrueLeft() throws Exception {
            //assertTransform("true or a", "true");
    	String entrada = "TRUE O " + a +  ";";
    	String equivalente = "TRUE;";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }
    
    
    @Test
    public void booleanOrFalseLeft() throws Exception {
            //assertTransform("false or a", "(atom a)");
    	String entrada = "FALSE O " + a +  ";";
    	String equivalente = a +  ";";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }

    @Test
    public void booleanOrTrueRight() throws Exception {
            //assertTransform("a or true", "true");
    	String entrada =  a + " O TRUE;";
    	String equivalente = "TRUE;";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }

    @Test
    public void booleanOrFalseRight() throws Exception {
            //assertTransform("a or false", "(atom a)");
    	String entrada =  a + " O FALSE;";
    	String equivalente = a +  ";";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }
    
    @Test
    public void notBooleanTrue() throws Exception {
            //assertTransform("not true", "false");
    	String entrada = "NO TRUE;";
    	String equivalente = "FALSE;";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }

    @Test
    public void notBooleanFalse() throws Exception {
            //assertTransform("not false", "true");
    	String entrada = "NO FALSE;";
    	String equivalente = "TRUE;";
    	
    	assertEquals(transforma(entrada), transforma(equivalente));
    }
    
    
    private String transforma(String entrada) throws IOException {
    	
    	StringReader sr = new StringReader(entrada);
    	
		final ANTLRInputStream is = new ANTLRInputStream(sr);
        final logpropLexer lexer = new logpropLexer(is);
        final CommonTokenStream ts = new CommonTokenStream(lexer);
        final logpropParser parser = new logpropParser(ts);
        final FormulasContext formulas = parser.formulas();
        
        final logpropBaseVisitor<IASTNode> visitor = new ASTVisitor();
        final IASTNode astTree = visitor.visit(formulas);
        final IVisitor<IASTNode> fncVisitor = new FNCVisitor();
        final IASTNode fncTree = fncVisitor.visit(astTree);
        
        return fncTree.toString();
    }

}
